from  common import definesymbols
from automatadefs import *
from graphics import draw
from operations import product,kleeneclosuregen,ac,coac
from diagnosis import diagnoser,labelfailaut,observerdelta
EMPTYSET = set([])




#def projectiondelta(self,Eo=EMPTYSET):
#    
#    if Eo == EMPTYSET:
#        sigmaObs = self.Eobs
#    else:
#        if isinstance(Eo,set):
#            sigmaObs = Eo
#        elif isinstance(Eo,list):
#            sigmaObs = set(Eo)
#        else:
#            raise invalidArgument, 'Observed set must be of type set or list'
#                    
#    delta='\Delta'          
#    auto=self.copy()
#    graph= auto.nxGraph    
#    sigma = auto.E    
#    X0 = list(auto.X0)
#    Xwaiting = list(auto.X0)
#    Xdone=EMPTYSET
#    Xm=EMPTYSET
#    existunobsCycle = False
#    
#        
#    def unobs_reach_states(state):
#        Xvisited=[state]
#        Xreachable = set([state]) 
#        unobsCycle = False      
#        while  Xvisited <> []:
#            xcurrent = Xvisited.pop()  
#            for edge in graph.out_edges_iter(xcurrent,keys=True):
#                event = edge[2]
#                next_xcurrent = edge[1]
#                if (event not in sigmaObs):
#                    if next_xcurrent not in Xreachable:
#                        Xvisited.append(next_xcurrent)                  
#                        Xreachable = Xreachable|set([next_xcurrent])
#                    elif event == delta:
#                        unobsCycle = True 
#                    else:
#                        unobsCycle = True                                                
#        return Xreachable, unobsCycle   
#   
#   
#    
#    while Xwaiting <> [] :
#        
#        xcurrent = Xwaiting.pop();
#        Xdone = Xdone | set([xcurrent])
#        Xuobsreach,unobsCycle = unobs_reach_states(xcurrent)
#        
#        
#        for edge in graph.out_edges_iter(xcurrent,keys=True):
#            event = edge[2]
#            next_xcurrent = edge[1]
#            if event not in sigmaObs:
#                graph.remove_edge(xcurrent,next_xcurrent, key = event)
#                
#        for xreach in Xuobsreach:
#            for edge in graph.out_edges_iter(xreach,keys=True):
#                next_xreach=edge[1]
#                event = edge[2]
#                if event in sigmaObs:  
#                    graph.add_edge(xcurrent,next_xreach, key=event, label=event)
#                    if next_xreach not in Xdone:             
#                        Xwaiting.append(next_xreach)
#            if xreach in auto.Xm:
#                Xm = Xm | set([xcurrent])
#        if unobsCycle:
#            graph.add_edge(xcurrent,xcurrent, key=delta, label=delta)
#            existunobsCycle = True
#        
#        reachableStates = nx.algorithms.traversal.depth_first_search.dfs_tree(graph,X0[0])
#        reachableStates = set(reachableStates)
#        auto.nxGraph.remove_nodes_from(auto.X-reachableStates)
#        auto.X = set(reachableStates) 
#        if existunobsCycle:
#            auto.E = sigmaObs|set([delta])
#        else:
#            auto.E = sigmaObs
#        auto.Eobs = sigmaObs
#        auto.gammaDict,auto.deltaDict,auto.infoDict=create_FSA_transdicts(auto.nxGraph,auto.X,auto.E,auto.X0)     
#        auto.nxDigraph=Create_nxDigraph(auto)
#    
#    return auto
# 
#
#def projectiondelta(self,Eo=EMPTYSET):
#    
#    if Eo == EMPTYSET:
#        sigmaObs = self.Eobs
#    else:
#        if isinstance(Eo,set):
#            sigmaObs = Eo
#        elif isinstance(Eo,list):
#            sigmaObs = set(Eo)
#        else:
#            raise invalidArgument, 'Observed set must be of type set or list'
#                    
#    delta='\Delta'          
#    auto=self.copy()
#    graph= auto.nxGraph    
#    sigma = auto.E    
#    X0 = list(auto.X0)
#    Xwaiting = list(auto.X0)
#    Xdone=EMPTYSET
#    Xm=EMPTYSET
#    existunobsCycle = False
#    
#        
#    def unobsreach(state):
#        Xvisited=[state]
#        Xreachable = set([state]) 
#        unobsCycle = False      
#        while  Xvisited <> []:
#            xcurrent = Xvisited.pop()  
#            for edge in graph.out_edges_iter(xcurrent,keys=True):
#                event = edge[2]
#                next_xcurrent = edge[1]
#                if (event not in sigmaObs):
#                    if next_xcurrent not in Xreachable:
#                        Xvisited.append(next_xcurrent)                  
#                        Xreachable = Xreachable|set([next_xcurrent])
#                    elif event == delta:
#                        unobsCycle = True 
#                    else:
#                        unobsCycle = True                                                
#        return Xreachable, unobsCycle   
#   
#   
#    
#    while Xwaiting <> [] :
#        
#        xcurrent = Xwaiting.pop();
#        Xdone = Xdone | set([xcurrent])
#        Xuobsreach,unobsCycle = unobsreach(xcurrent)
#        
#        
#        for edge in graph.out_edges_iter(xcurrent,keys=True):
#            event = edge[2]
#            next_xcurrent = edge[1]
#            if event not in sigmaObs:
#                graph.remove_edge(xcurrent,next_xcurrent, key = event)
#                
#        for xreach in Xuobsreach:
#            for edge in graph.out_edges_iter(xreach,keys=True):
#                next_xreach=edge[1]
#                event = edge[2]
#                if event in sigmaObs:  
#                    graph.add_edge(xcurrent,next_xreach, key=event, label=event)
#                    if next_xreach not in Xdone:             
#                        Xwaiting.append(next_xreach)
#            if xreach in auto.Xm:
#                Xm = Xm | set([xcurrent])
#        if unobsCycle:
#            graph.add_edge(xcurrent,xcurrent, key=delta, label=delta)
#            existunobsCycle = True
#        
#        reachableStates = nx.algorithms.traversal.depth_first_search.dfs_tree(graph,X0[0])
#        reachableStates = set(reachableStates)
#        auto.nxGraph.remove_nodes_from(auto.X-reachableStates)
#        auto.X = set(reachableStates) 
#        if existunobsCycle:
#            auto.E = sigmaObs|set([delta])
#        else:
#            auto.E = sigmaObs
#        auto.Eobs = sigmaObs
#        auto.gammaDict,auto.deltaDict,auto.infoDict=create_FSA_transdicts(auto.nxGraph,auto.X,auto.E,auto.X0)     
#        auto.nxDigraph=Create_nxDigraph(auto)
#    
#    return auto
 
 


#def observer(self,Eo=EMPTYSET):
#    from automatadefs import fsa
#
#    X0, X, E, gamma  = self.X0, self.X, self.E,self.gamma,     
#    Xm, type, name, = self.Xm, self.type,self.name, 
#       
#    if Eo <> EMPTYSET :
#        if isinstance(Eo,list):
#            Eunobs = self.E-set(Eo)
#            Eobs = self.E-Eunobs 
#        elif isinstance(Eo,set):
#            Eunobs=self.E-Eo
#            Eobs = self.E-Eunobs 
#        else: raise invalidArgument, 'Observable event set must be of type set or list'
#    else:
#        Eunobs = self.E-self.Eobs
#        Eobs = self.Eobs
#                   
#    if (self.isDFA() &  ( Eobs == self.E)):
#        return self 
#    
#    
#    def delta_one_event(state,event): 
#        
#        if event in self.gamma(state):
#            return self.deltaDict[state][event]
#        else: 
#            return EMPTYSET
#    
#       
#    def extended_gamma(setState):                              
#        activeEvents = EMPTYSET
#        for state in setState:
#            activeEvents=activeEvents | self.gamma(state)
#        activeEvents=activeEvents#-set([epsilon])
#        return activeEvents
#    
#    def convertname(stateObserved):
#      
#        stateObserved=list(stateObserved)
#        stateObserved.sort()
#        nameState=''            
#        for atomicState in stateObserved:
#            nameState=nameState+str(atomicState)+','        
#        nameState='\{'+nameState.rstrip(',')+'\}'          
#        return nameState    
#    
#    def unobsreach(setStates):
#                    
#        Xwaiting=list(setStates)
#        Xreachable=setStates
#     
#        while Xwaiting <> []:
#            reachedState = Xwaiting.pop()
#            nextReachSet = EMPTYSET             
#            for sigma in Eunobs:               
#                nextReachSet = nextReachSet | delta_one_event(reachedState,sigma)
#            for next_xcurrent in nextReachSet:               
#                if next_xcurrent not in Xreachable:
#                    Xreachable = Xreachable | set([next_xcurrent])
#                    Xwaiting.append(next_xcurrent)                    
#        return Xreachable       
#    
#    
#    def delta_ext_unobservable(state,event):
#                                      
#        unobsReachSet =unobsreach(state) 
#        nextReachedSet=EMPTYSET                           
#        for reachState in unobsReachSet:
#            nextReachedSet=nextReachedSet | delta_one_event(reachState,event)    
#        unobsReachSet,unobsCycle =unobsreach(nextReachedSet)             
#        return unobsReachSet   
#   
# 
#     
#    X0obs = self.unobsreach(X0)
#    Xobs = [X0obs]
#    Xwaiting = [X0obs]
#    transition = []
#    X0obsname=convertname(X0obs)
#    
#    while Xwaiting <> []:
#        stateSet=Xwaiting.pop()                     
#        validSet = extended_gamma(stateSet) & (Eobs)
#        for sigma in validSet:
#            nextState=self.delta(stateSet,sigma)
#            if nextState not in Xobs: 
#                Xobs.append(nextState)
#                Xwaiting.append(nextState) 
#            transition.append([convertname(stateSet),sigma,convertname(nextState)])
#    
#    Xmobs,Xobsname = [], []   
#    StateLabel = {} 
#       
#    for observedState in Xobs:
#        nameState=convertname(observedState)
#        Xobsname.append(nameState)
#        if (observedState & Xm) <> EMPTYSET:
#            nameState=convertname(observedState)
#            Xmobs.append(nameState)
#          
#    nameobs = 'observer'       
#    auto = fsa(Xobsname,self.Eobs, transition,X0obsname,Xmobs, Eobs =self.Eobs,
#                Econ = self.Econ,name=nameobs,type='observer') 
#    auto.style='observer'
#    auto.direction='UD'
#    return auto 


a,b,c,d,e,sf,x0,x1,x2,x3,x4,x5,x6,x7 = definesymbols('a b c d e \sigma_f 0 1 2 3 4 5 6 7')
a,b,c,d,e,sf,x0,x1,x2,x3,x4,x5,x6,x7 = definesymbols('a b c d e \sigma_f 0 1 2 3 4 5 6 7')

sigma=set([a,b,c,d,e,sf])
sigmaf=set([sf])
X=[x1,x2,x3,x4,x5,x6,x7]
X0=[x1]
Xm=[x1,x7]
transicoes=[[x1,c,x2],[x1,a,x5],[x2,sf,x3],[x3,e,x4],
            [x4,d,x4],[x1,a,x5],[x5,b,x6],[x6,d,x6],[x7,e,x7],[x3,a,x7]]
sigmaobs=[a,b,c,d]
G=fsa(X,sigma,transicoes,X0,Xm,Eobs=sigmaobs,name='$G$') 

D=diagnoser(G,sf,sigmaobs)




def dilatation(G,sigmaisf):
    G_dilated = G.copy()
    for state in G.X:
        for event in G.gamma(state):
            if event in sigmaisf:
                next_state=G.delta(state,event)
                event_no = event + "'"
                G_dilated = G_dilated.addtransition([state,event_no,next_state])             
    return G_dilated
                
#draw(G)
isf=[b,c]
D=dilatation(G,isf)
draw(G,D)
